\section{Zeno's proof output}
\label{sec:proof}

In this section we explain Zeno's proof output using the example proof in \fig{proofaddzero}. Zeno's output is a textual representation of the proof tree constructed by Zeno, where each line is a node in the tree. The topmost node of the tree and the first line of our output is  the property we are trying to prove.

Zeno  uses indentation and line breaks to represent the tree structure. Thus, a node with one child is separated from its child by a new line, and appears at the same
indentation level as the child. For example, the node at line 3 has a unique child which appears on line 4.
A node with multiple children (or, in other words, a node with multiple branches) is represented by indentation for each branch, and by separating the branches by an empty line. For example, the node at line 1 has two children, one at line 3 and the other at line 7.
Each line of the proof output %, and so each node in the proof tree,
contains  % two pieces of information:
  the \emph{proof step}   taken to reach this line from its parent  and is given in square brackets \li{[...]}
 at the start of the line (these steps are explained in the next Section),
 % \ref{sec:steps}),
 and  the property that is to be proven (\li{True} indicates that the proof branch is complete).

The parent relationship expresses entailment; in other words, the property at a node is a consequence of the conjunction of the properties of all its children. For example,
\li{0 + 0 = 0} from line 3 is a consequence of \li{0 = 0}  from line 4. Similarly, the property \li{x + 0 = x} from line 1 is a consequence of the conjunction of  \li{0 + 0 = 0} from line 3 and of $\lim{x' + 0 = x} \Rightarrow \lim{S x' + 0 = S x'}$  from line 7. (Note that the \li{with} on line 8 shows we have added a property to our list of inductive hypotheses down this branch and is always part of a previous inductive step.)

At the end of the output Zeno gives all the auxiliary lemmas 
that it has proven.
For example, as we see on line 19 of \fig{proofmaxzero},
in order to prove that \li{0} is a right-identity for \li{max},
Zeno discovers and proves  the auxiliary lemma that \li{0} is
the only number less than or equal to \li{0}.

\begin{figure}
\small
\begin{lstlisting}[numbers=left]
[goal] x + 0 = x

 > [ind x => 0] 0 + 0 = 0
 > [def] 0 = 0
 > [eql] True

 > [ind x => S x'] S x' + 0 = S x'
     with x' + 0 = x'
 > [def] S (x' + 0) = S x'
 > [hyp x' + 0 = x'] S x' = S x'
 > [eql] True

Proven: x + 0 = x
\end{lstlisting}
\caption{Zeno's proof that \li{+} is a right-identity for \li{(+)}}
\label{fig:proofaddzero}
\end{figure} 